Example 1 in [Lucas - RTA'02]

Summary: Ex1_Luc02b

• CS-TRS format
• OBJ format
• Negative results:
  1. Lucas' transformation (Extra variables)
• Positive results:
  1. Zantema's transformation (RPOS @ AProVE)
  2. Ferreira and Ribeiro's transformation (Corollary)
  3. Giesl and Middeldorp's transformation (Corollary)
  4. CSRPO
  5. Polynomial interpretation

CS-TRS Ex1_Luc02b (file Ex1_Luc02b.csr)

Functions:  from cons s first 0 nil sel

Constructors:  cons s 0 nil

Variables:  X Z Y

Arities: 

ar(from) = 1
ar(cons) = 2
ar(s) = 1
ar(first) = 2
ar(0) = 0
ar(nil) = 0
ar(sel) = 2

Replacement map: 

µ(from)={1}
µ(cons)={1}
µ(s)={1}
µ(first)={1,2}
µ(0)={}
µ(nil)={}
µ(sel)={1,2}

Rules: (file Ex1_Luc02b) 

from(X) -> cons(X,from(s(X)))
first(0,Z) -> nil
first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z))
sel(0,cons(X,Z)) -> X
sel(s(X),cons(Y,Z)) -> sel(X,Z)

The CS-TRS in OBJ format (file Ex1_Luc02b.obj):

obj Ex1_Luc02b is
  sort S .
  op from : S -> S .
  op cons : S S -> S [strat (1 0)] .
  op s : S -> S .
  op first : S S -> S .
  op 0 : -> S .
  op nil : -> S .
  op sel : S S -> S .
  vars X Z Y : S .
  eq from(X) = cons(X,from(s(X))) .
  eq first(0,Z) = nil .
  eq first(s(X),cons(Y,Z)) = cons(Y,first(X,Z)) .
  eq sel(0,cons(X,Z)) = X .
  eq sel(s(X),cons(Y,Z)) = sel(X,Z) .
endo

Negative results

1. The µ-termination of Ex1_Luc02b cannot be proved by using Lucas' transformation. The TRS Ex1_Luc02b_L:

       from(X) -> cons(X)
       first(0,Z) -> nil
       first(s(X),cons(Y)) -> cons(Y)
       sel(0,cons(X)) -> X
       sel(s(X),cons(Y)) -> sel(X,Z)
       

   contains extra variables.

Positive results

1. Ex1_Luc02b is proved µ-terminating in [Luc02b, Example 8] by using Zantema's transformation. The TRS Ex1_Luc02b_Z:

       from(X) -> cons(X,n__from(s(X)))
       first(0,Z) -> nil
       first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z)))
       sel(0,cons(X,Z)) -> X
       sel(s(X),cons(Y,Z)) -> sel(X,activate(Z))
       from(X) -> n__from(X)
       first(X1,X2) -> n__first(X1,X2)
       activate(n__from(X)) -> from(X)
       activate(n__first(X1,X2)) -> first(X1,X2)
       activate(X) -> X
       

   is terminating (use RPOS with AProVE).
2. By [GM04, Theorem 11], the µ-termination of Ex1_Luc02b can also be proved by using Ferreira and Ribeiro's transformation (but no concrete proof has been reported yet).
3. By [GM04, Theorem 22], the µ-termination of Ex1_Luc02b can also be proved by using Giesl and Middeldorp's transformation (but no concrete proof has been reported yet).
4. The µ-termination of Ex1_Luc02b can be proved by CSRPO together with the following . [BLR02, Example 7] and automatically by MuTerm:
   • marking map:

            m(cons,2)=m(_cons,2)={from}
            

   • precedence:

            first > from, nil, cons
            sel > from > cons, s, _from
            

   • status:

            st(first)=st(sel)=lex; 
            st(f)=mul for all other symbols f.
            

5. The µ-termination of Ex1_Luc02b can be proved by using a polynomial interpretation over Q_1:

      [from](x) = 2x + 2
      [cons](x,y) = x + y/4
      [s](x) = 2x
      [first](x,y) = x + y + 1
      [0] = 1
      [nil] = 1
      [sel](x,y) = (x^2)y + 1